i:Id, k:Knd, l:IdLnk, ds:x:Id fp Type, da:ltg:Knd fp Type,
f:((tg:Id  (State(ds)Valtype(da;k)(da(rcv(l,tg))?Void List))) List).
@i: with declarations ds:dsda:da k(v) sends f s v on link l  Dsys 

latex

Definitions	x:A. B(x), t  T, Dsys, @i: with declarations ds:dsda:da k(v) sends f s v on link l, x. t(x), x(s)
Lemmas	ifthenelse wf, eqof wf, Id wf, id-deq wf, msga wf, ma-single-sends wf, ma-empty wf, ma-state wf, ma-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf, fpf wf, IdLnk wf